#include "eval.hh"

#include <exception>

//Implementation of the EX operator.
bdd
bdd_EX (bdd f, Model& model)
{
  bdd predecessors = compute_predecessors(f, model);

  return predecessors;
}

//Implementation of the AX operator.
bdd
bdd_AX (bdd f, Model& model)
{
  bdd result = compute_not(
			   bdd_EX(compute_not(f, model),
				  model),
			   model);

  return result;
}

//Implementation of the AF operator.
bdd
bdd_AF (bdd f, Model& model)
{
  bdd old;

  do
    {
      old = f;
      f |= bdd_AX(f, model);
    }
  while (old != f);

  return f;
}


//Implementation of the EF operator.
bdd
bdd_EF (bdd f, Model& model)
{
  bdd old;

  do
    {
      old = f;
      f |= bdd_EX(f, model);
    }
  while (old != f);

  return f;
}

//Implementation of the AG operator.
bdd
bdd_AG (bdd f, Model& model)
{
  bdd old;

  do
    {
      old = f;
      f &= bdd_AX(f, model);
    }
  while (old != f);

  return f;
}


//Implementation of the EG operator.
bdd
bdd_EG (bdd f, Model& model)
{
  bdd old;

  do
    {
      old = f;
      f &= bdd_EX(f, model);
    }
  while (old != f);

  return f;
}

//Implementation of the AU operator.
bdd
bdd_AU (bdd f, bdd g, Model& model)
{
  bdd old;

  bdd res;

  do
    {
      old = res;
      res = g | (f & bdd_AX(res, model));
    }
  while (old != res);

  return res;
}

//Implementation of the EU operator.
bdd
bdd_EU (bdd f, bdd g, Model& model)
{
  bdd old;

  bdd res;

  do
    {
      old = res;
      res = g | (f & bdd_EX(res, model));
    }
  while (old != res);

  return res;
}

bdd
eval (AST*	formula,
      Model&	model)
{
  symbols val = formula->getValue ();

  if (val == AND)
    return bdd_and (eval (formula->getIthSon (0), model), eval (formula->getIthSon (1), model));

  if (val == OR)
    return bdd_or (eval (formula->getIthSon (0), model), eval (formula->getIthSon (1), model));

  if (val == NOT)
    return compute_not (eval (formula->getIthSon (0), model), model);

  if (val == IMPLIES)
    return bdd_imp (eval (formula->getIthSon (0), model), eval (formula->getIthSon (1), model));

  if (val == EX)
    return bdd_EX (eval (formula->getIthSon (0), model), model);

  if (val == AX)
    return bdd_AX (eval (formula->getIthSon (0), model), model);

  if (val == AF)
    return bdd_AF (eval (formula->getIthSon (0), model), model);

  if (val == EF)
    return bdd_EF (eval (formula->getIthSon (0), model), model);

  if (val == AG)
    return bdd_AG (eval (formula->getIthSon (0), model), model);

  if (val == EG)
    return bdd_EG (eval (formula->getIthSon (0), model), model);

  if (val == AU)
    return bdd_AU (eval (formula->getIthSon (0), model), eval (formula->getIthSon (1), model), model);

  if (val == EU)
    return bdd_EU (eval (formula->getIthSon (0), model), eval (formula->getIthSon (1), model), model);

  if (val == T)
    return bddtrue;

  if (val == F)
    return bddfalse;

  if (val == VAR)
    {
      std::string varname = formula->getVariable ();

      bool is_not = varname[0] == '~';
      
      if (is_not)
	varname.erase(0,1);

      int var_index = model.get_problem_variable_index(varname);

      if (var_index < 0)
	throw UnknownVariableException(varname);

      bdd var;
      if (is_not)
	var = bdd_nithvar(var_index);
      else
	var = bdd_ithvar(var_index);

      return compute_validating_states(var, model);
    }
}
